Lambda the Ultimate

In the continuing story called Epigram, a new contribution by James mcKinna and Joel Wright.

Conventional approaches to compiler correctness, type safety and type preservation have focused on off-line proofs, either on paper or formalised with a machine, of existing compilation schemes with respect to a reference operational semantics. This pearl shows how the use of dependent types in programming, illustrated here in Epigram, allows us not only to build-in these properties, but to write programs which guarantee them by design and subsequent construction.
We focus here on a very simple expression language, compiled into tree-structured code for a simple stack machine. Our purpose here is not to claim any sophistication in the source language being modelled, but to show off the metalanguage as a tool for writing programs for which the type preservation and progress theorems are self-evident by construction, and finally, whose correctness can be proved directly in the system.
In this simple setting we achieve the following;
• a type-preserving evaluation semantics, which takes typed expressions to typed values.
• a compiler, which takes typed expressions to stack-safe intermediate code.
• an interpreter for compiled code, which takes stack-safe intermediate code to a big-step
stack transition.
• a compiler correctness proof, described via a function whose type expresses the equational
correctness property.

P.S. I found it difficult to classify this paper correctly. Neither functional, nor type theory seem the proper category for a dependently typed programming language, which probably is a separate paradigm.

Ralf Lämmel and Erik Meijer. Revealing the X/O impedance mismatch.

When engaging in X/O mapping, i.e., when viewing XML data as objects or vice versa, one faces various conceptual and technical challenges -- they may be collectively referred to as the `X/O impedance mismatch'. There are these groups of challenges. (i) The XML data model and the object data model differ considerably. (ii) The native XML programming model differs from the normal OO programming model. (iii) The typical type systems for XML and objects differ considerably, too. (iv) Some of the differences between data models and between type systems are more like idiosyncrasies on the XML site that put additional burden on any X/O mapping effort. (v) In some cases, one could ask for slightly more, not necessarily XML-biased language expressiveness that would improve X/O mapping results or simplify efforts.

The present article systematically investigates the mismatch in depth. It identifies and categorizes the various challenges. Known mitigation techniques are documented and assessed; several original techniques are proposed. The article is somewhat biased in that it focuses on XML Schema as the XML type system of choice and on C# as the OO programming language of choice. In fact, XSD and C# are covered quite deeply. Hence, the present article qualifies as a language tutorial of `the other kind'.

This paper is over 100 pages, way longer than I have the time to read at the moment. Skimming, the paper looks interesting and useful. If you manage to read the whole thing, do share your observations with us in the discussion group.

This blog aims to address all aspects of DSL development, focussing particularly on DSLs embedded in Ruby.

If our DSL department isn't enough for you, you might want to check out this newcomer.

While you wait to see how this blog turns out, you might want to browse our DSL archive: here and here (we also have a fairly empty Ruby department, by the way). After all, we've been doing this for nearly six years now!

Welcome to blogosphere, Dave & Tobias!

The presentation slides for this Ada-Europe paper are online (the paper itself is proabably behind a paywall). The authors are Ben Brosgol from AdaCore and Andy Wellings from the University of York (UK) , really the guys to read if you are interested in these topics.

Some of the issues alluded to in the slides were discussed here in the past, either in general discussions about Ada or in discussions about the specific issues (RTSJ, async transfer of control etc.)

Tim Harris. Leaky regions: linking reclamation hints to program structure. June 2006 Microsoft Research Technical Report MSR-TR-2006-84.

This paper presents a new mechanism for automatic storage reclamation based on exploiting information about the relationship between object lifetimes and points in a program's execution. In our system method calls are annotated to indicate that most of the objects allocated during the call are expected to be unreachable by the time it returns. A write barrier detects if objects escape from one of these calls, causing them to be retained and subsequently managed by an ordinary generational collector. We describe a tool that helps select suitable annotation sites and we outline how this process can be fully automated. We show that if these annotations are placed judiciously then the additional costs of the write barrier can be outweighed by savings in collection time.

Not really my area of interest, but since there was much discussion about GC and related topics in the discussion group I thought I'd post a link to this tech report.

Interesting draft paper on the History of Haskell by Simon Peyton Jones, Phil Wadler, Paul Hudak, and John Hughes.

This paper describes the history of Haskell, including its genesis and principles, technical contributions, implementations and tools, and applications and impact.

This paper is aimed at History of Programming Languages - HOPL III to be held in June 2007.

In 1978, the first History of Programming Language Conference (HOPL) described the development of 13 computer programming languages, the people who participated in that work, and the context in which it was undertaken. In 1993, HOPL-II contained 14 papers on the genesis and evolution of programming languages. It is time for HOPL-III, to be held with FCRC 2007 in San Diego. Each HOPL-III paper should detail the early history or evolution of a specific programming language. Preliminary ideas about each language should have been documented by 1996 and each language should have been in use by 1998.

Which leaves the question of which PLs should take part in HOPL-III?
(I guess I need to go back and remember which were documentend in I & II).

A Core Calculus for Scala Type Checking, is a new paper by the Scala team.

Abstract. We present a minimal core calculus that captures interesting constructs of the Scala programming language: nested classes, abstract types, mixin composition, and path dependent types. We show that the problems of type assignment and subtyping in this calculus are decidable.

The paper revolves around the question of decidability of type checking in Scala. The following quote summarizes the background of this question.

Scala’s approach to component modeling is based on three programming language constructs: modular mixin composition, abstract type members, and explicit self-types. All three have been studied in the vObj calculus. A key concept of the vObj calculus, path-dependent types, is also present in Scala. However, some other constructions of vObj do not correspond to Scala language constructs. In particular, vObj has first-class classes which can be passed around as values, but Scala has not.
First-class classes were essential in establishing an encoding of F<: in vObj, which led to a proof of undecidability of vObj by reduction to the same property in F<:. However, since Scala lacks first-class classes, the undecidability result for the calculus does not imply that type checking for the programming language is undecidable.

Ehud: Given current interest in Scala and its more or less unique (don't want to raise controversy here) position as being both a functional and an OO language, furthermore being much more than a toy language, would it be a good idea to give Scala a place in the Spotlight section?

History of LISP (software collection committee) edited by Paul McJones. Abstract:

The goal of this project is to locate source code, design documents, and other materials concerning the original LISP I/1.5 system, and as many of its follow-ons as possible. LISP was one of the earliest high-level programming languages and introduced many ideas such as garbage collection, recursive functions, symbolic expressions, and dynamic type-checking. This is a pilot project of the Computer History Museum's Software Collection Committee to develop expertise in the collection, preservation, and presentation of historic software. Comments, suggestions, and donations of additional materials are greatly appreciated.

I ran across this page by accident while googling for "lisp assembler lap" because I'd recently learned LAP was the standard acronym for lisp assembly program (ie a lisp based assember), which also described what I was currently trying to do. It's funny how often a new idea is just the Nth repetition of many old ideas. :-)

Anyway, this page links a wealth of interesting material on early Lisp implementations. (Unfortunately a number of the PDF documents don't open on my current machine, so I can't read several of the items I find most interesting, including everything L. Peter Deutsch authored.)

While on the subject of quantum computing, I think some of you might enjoy playing with this Scheme DSEL for quantum computation from André van Tonder.

Peter Selinger. A brief survey of quantum programming languages.
In Proceedings of the 7th International Symposium on Functional and Logic Programming, Nara, Japan. Springer LNCS 2998, pp. 1-6, 2004.

A brief but useful survey of quantum programming languages (six pages), that I think wasn't mentioned here before.

Section 2.1 describes the common target hardware models (the quantum circuit model, QRAM, and quantum Turing Machines).

Section 2.2 is about imperative quantum languages (e.g., QCL), and section 2.3 discusses functional quantum languages.